T:Type, eq:EqDecider(T), a:T, L:T List.
(b:T. (b  insert(a;L))  b = a  (b  L)) & (no_repeats(T;L)  no_repeats(T;insert(a;L))) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), no_repeats(T;l), (x  l), Prop, P  Q, insert(a;L), P  Q, P  Q, P & Q, P  Q, A, hd(l), i<j, ij, l[i], b, Unit, , tl(l), b, if b t else f fi, nth_tl(n;as), Y, ||as||, AB, , deq-member(eq;x;L), {T}, True, T
Lemmas	no repeats cons, squash wf, true wf, cons member, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, insert wf, l member wf, no repeats wf, deq wf